x:Knd, T:Type. normal-type{i:l}(T)  normal-da{i:l}(fpf-single(x; T)) 

latex

Definitions	t  T, guard(T), P  Q, x:A. B(x), sq_type(T), Knd, s = t, prop{i:l}, sqequal(s; t), left + right, void, isect(A; x.B(x)), top, Kind-deq, x:AB(x), x:A  B(x), P  Q, P  Q, x.A(x), x. t(x), fpf-single(x; v), fpf-dom(eq; x; f), b, fpf-ap(f; eq; x), normal-type{i:l}(T), fpf-all(A; eq; f; x,v.P(x;v)), normal-da{i:l}(da), Type
Lemmas	normal-type wf, assert wf, fpf-dom wf, fpf-single wf, top wf, fpf-single-dom, Kind-deq wf, Knd wf, Knd sq